The present invention relates generally to functional verification of circuit designs and, more particularly, to synthesis techniques used in constructing logic networks used in the functional verification process.
I. Description of the Related Art
Today, integrated circuits (ICs) typically contain large numbers of circuit elements. Computer-aided design (CAD) and computer-aided engineering (CAE) tools are essential in assisting circuit designers to produce these complicated ICs. Circuit designs are typically represented in a user-specified hardware description language (HDL), which demonstrate the functional properties of the circuit.
Designers commonly utilize CAE software to translate a HDL representation, which is typically in Register-Transfer-Level (RTL) description, into a gate-level netlist representation, and perform design validation to ensure that no design errors occurred in the process. With increasing design complexity, formal verification (equivalence checking) becomes integral in the design process to ensure that a refinement of the original specification (commonly referred to as revised circuit or design) is equivalent to the original specification (commonly referred to as golden circuit or design).
Conventional verification methods utilize Binary Decision Diagrams (BDDs) to represent the logic circuits involved in equivalence relationships. A primary drawback to using BDDs is their exponential memory complexity associated with large complex designs. The exponential memory complexity associated with using BDDs limits its applicability.
Various methods that attempt to address the deficiencies inherent in using BDDs have been presented. (See e.g., J. Jain, R. Mukherjee, and M. Fujita, Advanced Verification Techniques Based on Learning, Proc. 32nd ACM/IEEE DAC, June 1995, 420–26; W. Kunz, HANNIBAL: An Efficient Tool for Logic Verification Based on Recursive Learning, Proc. 1993 IEEE, Intl. Conf. On CAD, November 1993, 538–43; Y. Matsunaga, An Efficient Equivalence Checker for Combinatorial Circuits, Proc. 33rd ACM/IEEE DAC, June 1996, 629–34; A. Kuehlmann, F. Krohm, Equivalence Checking Using Cuts and Heaps, Proc. Int. Conf. Computer-Aided Design, 1997).
These techniques rely on the existence of intermediate functions that occur in the specification and in the implementation of the circuit design. The intermediate functions are utilized as cut points to partition a complex circuit network into a set of smaller and simpler comparisons. In general, there is a correlation between the number of cut points and equivalence checking performance. Therefore, it is preferable to create a golden circuit that is synthesized to have high structural similarity to the revised circuit to increase the possibility of obtaining more cut points. However, the aforementioned techniques fail to address generating golden circuits having a high number of cut points.
Thus, systems and methods for creating a golden circuit having high structural similarity to the revised circuit is desired. Verification systems incorporating synthesis methods that allow it to efficiently determine the architecture of a revised circuit, and subsequently use that knowledge to construct logic networks having an architecture closely resembling the revised circuit is also desired.